Nuprl Lemma : detach_wf
13,42
postcript
pdf
T
:Type,
A
:(
T
).
T
-Detach(
A
)
latex
Up
gen
algebra
1
Definitions of Statement
T
-Detach(
A
)
Definitions
T
-Detach(
A
)
,
t
T
,
,
x
:
A
.
B
(
x
)
Lemmas
decidable
wf
origin
T:Type, A:(T
). T-Detach(A) 
T:Type, A:(T). T-Detach(A) Tx:A. B(x)